Theorem 3impia 1224

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1217	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  mopick2  2161  3gencl  2834  mob2  2983  moi  2986  reupick3  3489  disjne  3545  elpr2elpr  3853  disji2  4074  tz7.2  4444  funopg  5351  fvun1  5699  fvopab6  5730  isores3  5938  ovmpt4g  6126  ovmpos  6127  ov2gf  6128  ofrval  6227  poxp  6376  smoel  6444  tfr1onlemaccex  6492  tfrcllemaccex  6505  nnaass  6629  qsel  6757  xpdom3m  6989  phpm  7023  ctssdc  7276  mkvprop  7321  prarloclem3  7680  aptisr  7962  axpre-apti  8068  axapti  8213  addn0nid  8516  divvalap  8817  letrp1  8991  p1le  8992  zextle  9534  zextlt  9535  btwnnz  9537  gtndiv  9538  uzind2  9555  fzind  9558  iccleub  10123  uzsubsubfz  10239  elfz0fzfz0  10318  difelfznle  10327  elfzo0le  10381  fzonmapblen  10383  fzofzim  10384  fzosplitprm1  10435  rebtwn2zlemstep  10467  qbtwnxr  10472  icogelb  10480  expcl2lemap  10768  expclzaplem  10780  expnegzap  10790  leexp2r  10810  expnbnd  10880  bcval4  10969  bccmpl  10971  elovmpowrd  11108  ccatval2  11128  wrdl1s1  11158  swrdsb0eq  11192  swrdccatin1  11252  pfxccatpfx2  11264  absexpzap  11586  divalgb  12431  ndvdssub  12436  dvdsgcd  12528  dfgcd2  12530  rplpwr  12543  nnmindc  12550  lcmgcdlem  12594  coprmdvds1  12608  qredeq  12613  prmdvdsexpr  12667  nnnn0modprm0  12773  pcexp  12827  difsqpwdvds  12856  prmpwdvds  12873  elrestr  13275  isnmgm  13388  grpasscan1  13591  grpinvnz  13599  mulgneg2  13688  dvdsrmul1  14060  dvdsunit  14070  lmodlema  14250  mopni  15150  sincosq1lem  15493  rpcxpmul2  15581  logbgcd1irr  15635  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem4  15737  2lgsoddprmlem3  15784  uhgredgrnv  15930  usgredg4  16007