Theorem 3impia 1203

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

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

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 983

This theorem is referenced by:  mopick2  2138  3gencl  2808  mob2  2957  moi  2960  reupick3  3462  disjne  3518  disji2  4043  tz7.2  4409  funopg  5314  fvun1  5658  fvopab6  5689  isores3  5897  ovmpt4g  6081  ovmpos  6082  ov2gf  6083  ofrval  6182  poxp  6331  smoel  6399  tfr1onlemaccex  6447  tfrcllemaccex  6460  nnaass  6584  qsel  6712  xpdom3m  6944  phpm  6977  ctssdc  7230  mkvprop  7275  prarloclem3  7630  aptisr  7912  axpre-apti  8018  axapti  8163  addn0nid  8466  divvalap  8767  letrp1  8941  p1le  8942  zextle  9484  zextlt  9485  btwnnz  9487  gtndiv  9488  uzind2  9505  fzind  9508  iccleub  10073  uzsubsubfz  10189  elfz0fzfz0  10268  difelfznle  10277  elfzo0le  10331  fzonmapblen  10333  fzofzim  10334  fzosplitprm1  10385  rebtwn2zlemstep  10417  qbtwnxr  10422  icogelb  10430  expcl2lemap  10718  expclzaplem  10730  expnegzap  10740  leexp2r  10760  expnbnd  10830  bcval4  10919  bccmpl  10921  elovmpowrd  11057  ccatval2  11077  wrdl1s1  11107  swrdsb0eq  11141  absexpzap  11466  divalgb  12311  ndvdssub  12316  dvdsgcd  12408  dfgcd2  12410  rplpwr  12423  nnmindc  12430  lcmgcdlem  12474  coprmdvds1  12488  qredeq  12493  prmdvdsexpr  12547  nnnn0modprm0  12653  pcexp  12707  difsqpwdvds  12736  prmpwdvds  12753  elrestr  13154  isnmgm  13267  grpasscan1  13470  grpinvnz  13478  mulgneg2  13567  dvdsrmul1  13939  dvdsunit  13949  lmodlema  14129  mopni  15029  sincosq1lem  15372  rpcxpmul2  15460  logbgcd1irr  15514  gausslemma2dlem1a  15610  gausslemma2dlem2  15614  gausslemma2dlem4  15616  2lgsoddprmlem3  15663