Theorem impl 460

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sbc2iedv  3820  csbie2t  3891  frinxp  5744  ordelord  6382  foco2  7104  f1ounsn  7270  frxp  8118  mpocurryd  8261  omsmolem  8639  erth  8745  unblem1  9248  unwdomg  9542  cflim2  10242  distrlem1pr  11005  uz11  12882  elpq  12994  xmulge0  13305  max0add  15357  lcmfunsnlem2lem1  16691  divgcdcoprm0  16718  cncongr1  16720  prmpwdvds  16959  imasleval  17590  issgrpd  18783  dfgrp3lem  19099  resscntz  19398  ablfac1c  20138  lbsind  21201  qsidomlem2  21481  isphld  21804  mplcoe5lem  22190  cply1mul  22456  smadiadetr  22832  chfacfisf  23011  chfacfisfcpmat  23012  chcoeffeq  23043  cayhamlem3  23044  tx1stc  23807  ioorcl  25736  coemullem  26407  xrlimcnp  27133  fsumdvdscom  27349  fsumvma  27377  cusgrres  29798  usgredgsscusgredg  29809  clwlkclwwlklem2a  30349  clwwlkext2edg  30407  frgrwopreglem5ALT  30673  frgr2wwlkeu  30678  frgr2wwlk1  30680  grpoidinvlem3  30858  htthlem  31269  atcvat4i  32749  abfmpeld  32999  ressupprn  33035  isarchi3  33507  ordtconnlem1  34314  gonarlem  35886  fmlasucdisj  35891  funpartfun  36435  relowlssretop  38029  ltflcei  38279  neificl  38424  keridl  38703  eqvrelth  39364  cvrat4  40237  ps-2  40272  mpaaeu  43897  clcnvlem  44369  fcoresf1  47826  modlt0b  48126  iccpartiltu  48191  2pwp1prm  48361  bgoldbtbnd  48594  isuspgrimlem  48680  grimedg  48720  grimgrtri  48734  lmod0rng  49014  lincext1  49254