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  3829  csbie2t  3899  frinxp  5745  ordelord  6383  foco2  7105  f1ounsn  7271  frxp  8122  mpocurryd  8265  omsmolem  8643  erth  8749  unblem1  9252  unwdomg  9546  cflim2  10247  distrlem1pr  11010  uz11  12887  elpq  12999  xmulge0  13310  max0add  15361  lcmfunsnlem2lem1  16696  divgcdcoprm0  16723  cncongr1  16725  prmpwdvds  16964  imasleval  17595  issgrpd  18788  dfgrp3lem  19104  resscntz  19403  ablfac1c  20143  lbsind  21179  qsidomlem2  21450  isphld  21773  mplcoe5lem  22159  cply1mul  22425  smadiadetr  22801  chfacfisf  22980  chfacfisfcpmat  22981  chcoeffeq  23012  cayhamlem3  23013  tx1stc  23776  ioorcl  25705  coemullem  26376  xrlimcnp  27099  fsumdvdscom  27315  fsumvma  27343  cusgrres  29739  usgredgsscusgredg  29750  clwlkclwwlklem2a  30290  clwwlkext2edg  30348  frgrwopreglem5ALT  30614  frgr2wwlkeu  30619  frgr2wwlk1  30621  grpoidinvlem3  30799  htthlem  31210  atcvat4i  32690  abfmpeld  32940  ressupprn  32976  isarchi3  33448  ordtconnlem1  34259  gonarlem  35819  fmlasucdisj  35824  funpartfun  36368  relowlssretop  37931  ltflcei  38181  neificl  38326  keridl  38605  eqvrelth  39268  cvrat4  40141  ps-2  40176  mpaaeu  43803  clcnvlem  44275  fcoresf1  47729  modlt0b  48029  iccpartiltu  48094  2pwp1prm  48264  bgoldbtbnd  48497  isuspgrimlem  48583  grimedg  48623  grimgrtri  48637  lmod0rng  48917  lincext1  49153