Theorem impl 455

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sbc2iedv  3819  csbie2t  3889  frinxp  5715  ordelord  6347  foco2  7063  f1ounsn  7228  frxp  8078  mpocurryd  8221  omsmolem  8595  erth  8700  unblem1  9204  unwdomg  9501  cflim2  10185  distrlem1pr  10948  uz11  12788  elpq  12900  xmulge0  13211  max0add  15245  lcmfunsnlem2lem1  16577  divgcdcoprm0  16604  cncongr1  16606  prmpwdvds  16844  imasleval  17474  issgrpd  18667  dfgrp3lem  18983  resscntz  19277  ablfac1c  20017  lbsind  21047  isphld  21624  mplcoe5lem  22009  cply1mul  22255  smadiadetr  22634  chfacfisf  22813  chfacfisfcpmat  22814  chcoeffeq  22845  cayhamlem3  22846  tx1stc  23609  ioorcl  25549  coemullem  26226  xrlimcnp  26949  fsumdvdscom  27166  fsumvma  27195  cusgrres  29538  usgredgsscusgredg  29549  clwlkclwwlklem2a  30089  clwwlkext2edg  30147  frgrwopreglem5ALT  30413  frgr2wwlkeu  30418  frgr2wwlk1  30420  grpoidinvlem3  30598  htthlem  31009  atcvat4i  32489  abfmpeld  32748  ressupprn  32784  isarchi3  33285  qsidomlem2  33550  ordtconnlem1  34106  gonarlem  35614  fmlasucdisj  35619  funpartfun  36163  relowlssretop  37622  ltflcei  37863  neificl  38008  keridl  38287  eqvrelth  38950  cvrat4  39823  ps-2  39858  mpaaeu  43511  clcnvlem  43983  fcoresf1  47433  modlt0b  47727  iccpartiltu  47786  2pwp1prm  47953  bgoldbtbnd  48173  isuspgrimlem  48259  grimedg  48299  grimgrtri  48313  lmod0rng  48593  lincext1  48818