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  3448  disjne  3504  disji2  4026  tz7.2  4389  funopg  5292  fvun1  5627  fvopab6  5658  isores3  5862  ovmpt4g  6045  ovmpos  6046  ov2gf  6047  ofrval  6146  poxp  6290  smoel  6358  tfr1onlemaccex  6406  tfrcllemaccex  6419  nnaass  6543  qsel  6671  xpdom3m  6893  phpm  6926  ctssdc  7179  mkvprop  7224  prarloclem3  7564  aptisr  7846  axpre-apti  7952  axapti  8097  addn0nid  8400  divvalap  8701  letrp1  8875  p1le  8876  zextle  9417  zextlt  9418  btwnnz  9420  gtndiv  9421  uzind2  9438  fzind  9441  iccleub  10006  uzsubsubfz  10122  elfz0fzfz0  10201  difelfznle  10210  elfzo0le  10261  fzonmapblen  10263  fzofzim  10264  fzosplitprm1  10310  rebtwn2zlemstep  10342  qbtwnxr  10347  icogelb  10355  expcl2lemap  10643  expclzaplem  10655  expnegzap  10665  leexp2r  10685  expnbnd  10755  bcval4  10844  bccmpl  10846  elovmpowrd  10976  absexpzap  11245  divalgb  12090  ndvdssub  12095  dvdsgcd  12179  dfgcd2  12181  rplpwr  12194  nnmindc  12201  lcmgcdlem  12245  coprmdvds1  12259  qredeq  12264  prmdvdsexpr  12318  nnnn0modprm0  12424  pcexp  12478  difsqpwdvds  12507  prmpwdvds  12524  elrestr  12918  isnmgm  13003  grpasscan1  13195  grpinvnz  13203  mulgneg2  13286  dvdsrmul1  13658  dvdsunit  13668  lmodlema  13848  mopni  14718  sincosq1lem  15061  rpcxpmul2  15149  logbgcd1irr  15203  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem4  15305  2lgsoddprmlem3  15352