Theorem 3impia 1202

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 1195	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 982

This theorem is referenced by:  mopick2  2128  3gencl  2797  mob2  2944  moi  2947  reupick3  3449  disjne  3505  disji2  4027  tz7.2  4390  funopg  5293  fvun1  5630  fvopab6  5661  isores3  5865  ovmpt4g  6049  ovmpos  6050  ov2gf  6051  ofrval  6150  poxp  6299  smoel  6367  tfr1onlemaccex  6415  tfrcllemaccex  6428  nnaass  6552  qsel  6680  xpdom3m  6902  phpm  6935  ctssdc  7188  mkvprop  7233  prarloclem3  7583  aptisr  7865  axpre-apti  7971  axapti  8116  addn0nid  8419  divvalap  8720  letrp1  8894  p1le  8895  zextle  9436  zextlt  9437  btwnnz  9439  gtndiv  9440  uzind2  9457  fzind  9460  iccleub  10025  uzsubsubfz  10141  elfz0fzfz0  10220  difelfznle  10229  elfzo0le  10280  fzonmapblen  10282  fzofzim  10283  fzosplitprm1  10329  rebtwn2zlemstep  10361  qbtwnxr  10366  icogelb  10374  expcl2lemap  10662  expclzaplem  10674  expnegzap  10684  leexp2r  10704  expnbnd  10774  bcval4  10863  bccmpl  10865  elovmpowrd  10995  absexpzap  11264  divalgb  12109  ndvdssub  12114  dvdsgcd  12206  dfgcd2  12208  rplpwr  12221  nnmindc  12228  lcmgcdlem  12272  coprmdvds1  12286  qredeq  12291  prmdvdsexpr  12345  nnnn0modprm0  12451  pcexp  12505  difsqpwdvds  12534  prmpwdvds  12551  elrestr  12951  isnmgm  13064  grpasscan1  13267  grpinvnz  13275  mulgneg2  13364  dvdsrmul1  13736  dvdsunit  13746  lmodlema  13926  mopni  14826  sincosq1lem  15169  rpcxpmul2  15257  logbgcd1irr  15311  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem4  15413  2lgsoddprmlem3  15460