Theorem impl 650

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
impl.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
impl	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem impl

Step	Hyp	Ref	Expression
1		impl.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 452	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 448	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  sbc2iedv  3506  csbie2t  3562  frinxp  5184  ordelord  5745  foco2  6379  foco2OLD  6380  frxp  7287  mpt2curryd  7395  omsmolem  7733  erth  7791  unblem1  8212  unwdomg  8489  cflim2  9085  distrlem1pr  9847  uz11  11710  xmulge0  12114  max0add  14050  lcmfunsnlem2lem1  15351  divgcdcoprm0  15379  cncongr1  15381  prmpwdvds  15608  imasleval  16201  dfgrp3lem  17513  resscntz  17764  ablfac1c  18470  lbsind  19080  mplcoe5lem  19467  cply1mul  19664  isphld  19999  smadiadetr  20481  chfacfisf  20659  chfacfisfcpmat  20660  chcoeffeq  20691  cayhamlem3  20692  tx1stc  21453  ioorcl  23345  coemullem  24006  xrlimcnp  24695  fsumdvdscom  24911  fsumvma  24938  cusgrres  26344  usgredgsscusgredg  26355  clwlkclwwlklem2a  26899  clwwlksext2edg  26923  frgrwopreglem5ALT  27186  frgr2wwlkeu  27191  frgr2wwlk1  27193  grpoidinvlem3  27360  htthlem  27774  atcvat4i  29256  abfmpeld  29454  isarchi3  29741  ordtconnlem1  29970  funpartfun  32050  relowlssretop  33211  ltflcei  33397  neificl  33549  keridl  33831  cvrat4  34729  ps-2  34764  mpaaeu  37720  clcnvlem  37930  iccpartiltu  41358  2pwp1prm  41503  bgoldbtbnd  41697  lmod0rng  41868  lincext1  42243