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  3815  csbie2t  3885  frinxp  5738  ordelord  6379  foco2  7103  f1ounsn  7274  frxp  8125  mpocurryd  8268  omsmolem  8648  erth  8754  unblem1  9265  unwdomg  9559  cflim2  10268  distrlem1pr  11037  uz11  12915  elpq  13028  xmulge0  13339  max0add  15400  lcmfunsnlem2lem1  16731  divgcdcoprm0  16758  cncongr1  16760  prmpwdvds  16999  imasleval  17630  issgrpd  18835  dfgrp3lem  19164  resscntz  19463  ablfac1c  20203  lbsind  21267  qsidomlem2  21547  isphld  21870  mplcoe5lem  22258  cply1mul  22524  smadiadetr  22900  chfacfisf  23082  chfacfisfcpmat  23083  chcoeffeq  23114  cayhamlem3  23115  tx1stc  23879  ioorcl  25808  coemullem  26479  xrlimcnp  27208  fsumdvdscom  27424  fsumvma  27452  cusgrres  29911  usgredgsscusgredg  29922  clwlkclwwlklem2a  30471  clwwlkext2edg  30529  frgrwopreglem5ALT  30805  frgr2wwlkeu  30810  frgr2wwlk1  30812  grpoidinvlem3  30990  htthlem  31401  atcvat4i  32881  abfmpeld  33130  ressupprn  33165  isarchi3  33630  ordtconnlem1  34437  gonarlem  35976  fmlasucdisj  35981  funpartfun  36525  relowlssretop  38120  ltflcei  38365  neificl  38506  keridl  38785  eqvrelth  39446  cvrat4  40319  ps-2  40354  mpaaeu  43994  clcnvlem  44466  fcoresf1  47960  modlt0b  48260  iccpartiltu  48325  2pwp1prm  48495  bgoldbtbnd  48728  isuspgrimlem  48814  grimedg  48854  grimgrtri  48868  lmod0rng  49147  lincext1  49387