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  2136  3gencl  2805  mob2  2952  moi  2955  reupick3  3457  disjne  3513  disji2  4036  tz7.2  4399  funopg  5302  fvun1  5639  fvopab6  5670  isores3  5874  ovmpt4g  6058  ovmpos  6059  ov2gf  6060  ofrval  6159  poxp  6308  smoel  6376  tfr1onlemaccex  6424  tfrcllemaccex  6437  nnaass  6561  qsel  6689  xpdom3m  6911  phpm  6944  ctssdc  7197  mkvprop  7242  prarloclem3  7592  aptisr  7874  axpre-apti  7980  axapti  8125  addn0nid  8428  divvalap  8729  letrp1  8903  p1le  8904  zextle  9446  zextlt  9447  btwnnz  9449  gtndiv  9450  uzind2  9467  fzind  9470  iccleub  10035  uzsubsubfz  10151  elfz0fzfz0  10230  difelfznle  10239  elfzo0le  10290  fzonmapblen  10292  fzofzim  10293  fzosplitprm1  10344  rebtwn2zlemstep  10376  qbtwnxr  10381  icogelb  10389  expcl2lemap  10677  expclzaplem  10689  expnegzap  10699  leexp2r  10719  expnbnd  10789  bcval4  10878  bccmpl  10880  elovmpowrd  11010  ccatval2  11029  absexpzap  11310  divalgb  12155  ndvdssub  12160  dvdsgcd  12252  dfgcd2  12254  rplpwr  12267  nnmindc  12274  lcmgcdlem  12318  coprmdvds1  12332  qredeq  12337  prmdvdsexpr  12391  nnnn0modprm0  12497  pcexp  12551  difsqpwdvds  12580  prmpwdvds  12597  elrestr  12997  isnmgm  13110  grpasscan1  13313  grpinvnz  13321  mulgneg2  13410  dvdsrmul1  13782  dvdsunit  13792  lmodlema  13972  mopni  14872  sincosq1lem  15215  rpcxpmul2  15303  logbgcd1irr  15357  gausslemma2dlem1a  15453  gausslemma2dlem2  15457  gausslemma2dlem4  15459  2lgsoddprmlem3  15506