Theorem impl 461

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbc2iedv  3823  csbie2t  3894  frinxp  5749  ordelord  6389  foco2  7111  f1ounsn  7281  frxp  8131  mpocurryd  8274  omsmolem  8652  erth  8758  unblem1  9262  unwdomg  9556  cflim2  10265  distrlem1pr  11028  uz11  12905  elpq  13017  xmulge0  13328  max0add  15387  lcmfunsnlem2lem1  16721  divgcdcoprm0  16748  cncongr1  16750  prmpwdvds  16989  imasleval  17620  issgrpd  18813  dfgrp3lem  19129  resscntz  19428  ablfac1c  20168  lbsind  21231  qsidomlem2  21511  isphld  21834  mplcoe5lem  22220  cply1mul  22486  smadiadetr  22862  chfacfisf  23041  chfacfisfcpmat  23042  chcoeffeq  23073  cayhamlem3  23074  tx1stc  23837  ioorcl  25766  coemullem  26437  xrlimcnp  27163  fsumdvdscom  27379  fsumvma  27407  cusgrres  29828  usgredgsscusgredg  29839  clwlkclwwlklem2a  30379  clwwlkext2edg  30437  frgrwopreglem5ALT  30703  frgr2wwlkeu  30708  frgr2wwlk1  30710  grpoidinvlem3  30888  htthlem  31299  atcvat4i  32779  abfmpeld  33029  ressupprn  33065  isarchi3  33531  ordtconnlem1  34338  gonarlem  35899  fmlasucdisj  35904  funpartfun  36448  relowlssretop  38042  ltflcei  38292  neificl  38437  keridl  38716  eqvrelth  39377  cvrat4  40250  ps-2  40285  mpaaeu  43910  clcnvlem  44382  fcoresf1  47839  modlt0b  48139  iccpartiltu  48204  2pwp1prm  48374  bgoldbtbnd  48607  isuspgrimlem  48693  grimedg  48733  grimgrtri  48747  lmod0rng  49027  lincext1  49267