Theorem impl 648

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 451	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 447	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sbc2iedv  3473  csbie2t  3528  frinxp  5107  ordelord  5662  foco2  6287  foco2OLD  6288  frxp  7174  mpt2curryd  7282  omsmolem  7620  erth  7678  unblem1  8097  unwdomg  8372  cflim2  8968  distrlem1pr  9726  uz11  11586  xmulge0  11986  max0add  13898  lcmfunsnlem2lem1  15189  divgcdcoprm0  15217  prmpwdvds  15446  imasleval  16024  dfgrp3lem  17336  resscntz  17587  ablfac1c  18293  lbsind  18901  mplcoe5lem  19288  cply1mul  19485  isphld  19818  smadiadetr  20300  chfacfisf  20478  chfacfisfcpmat  20479  chcoeffeq  20510  cayhamlem3  20511  tx1stc  21263  ioorcl  23151  coemullem  23810  xrlimcnp  24495  fsumdvdscom  24711  fsumvma  24738  clwlkisclwwlklem2a  26313  clwwlkext2edg  26330  frg2wot1  26584  grpoidinvlem3  26744  htthlem  27158  atcvat4i  28640  abfmpeld  28834  isarchi3  29072  ordtconlem1  29298  funpartfun  31220  relowlssretop  32387  ltflcei  32567  neificl  32719  keridl  33001  cvrat4  33747  ps-2  33782  mpaaeu  36739  clcnvlem  36949  iccpartiltu  39960  2pwp1prm  40041  bgoldbtbnd  40225  cusgrres  40664  usgredgsscusgredg  40675  clwlkclwwlklem2a  41207  clwwlksext2edg  41230  frgr2wwlk1  41494  lmod0rng  41658  lincext1  42037