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  3876  csbie2t  3949  frinxp  5771  ordelord  6408  foco2  7129  f1ounsn  7292  frxp  8150  mpocurryd  8293  omsmolem  8694  erth  8795  unblem1  9326  unwdomg  9622  cflim2  10301  distrlem1pr  11063  uz11  12901  elpq  13015  xmulge0  13323  max0add  15346  lcmfunsnlem2lem1  16672  divgcdcoprm0  16699  cncongr1  16701  prmpwdvds  16938  imasleval  17588  issgrpd  18756  dfgrp3lem  19069  resscntz  19364  ablfac1c  20106  lbsind  21097  isphld  21690  mplcoe5lem  22075  cply1mul  22316  smadiadetr  22697  chfacfisf  22876  chfacfisfcpmat  22877  chcoeffeq  22908  cayhamlem3  22909  tx1stc  23674  ioorcl  25626  coemullem  26304  xrlimcnp  27026  fsumdvdscom  27243  fsumvma  27272  cusgrres  29481  usgredgsscusgredg  29492  clwlkclwwlklem2a  30027  clwwlkext2edg  30085  frgrwopreglem5ALT  30351  frgr2wwlkeu  30356  frgr2wwlk1  30358  grpoidinvlem3  30535  htthlem  30946  atcvat4i  32426  abfmpeld  32671  ressupprn  32705  isarchi3  33177  qsidomlem2  33461  ordtconnlem1  33885  gonarlem  35379  fmlasucdisj  35384  funpartfun  35925  relowlssretop  37346  ltflcei  37595  neificl  37740  keridl  38019  eqvrelth  38593  cvrat4  39426  ps-2  39461  mpaaeu  43139  clcnvlem  43613  fcoresf1  47019  iccpartiltu  47347  2pwp1prm  47514  bgoldbtbnd  47734  isuspgrimlem  47812  grimedg  47841  grimgrtri  47852  lmod0rng  48073  lincext1  48300