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  4400  funopg  5304  fvun1  5644  fvopab6  5675  isores3  5883  ovmpt4g  6067  ovmpos  6068  ov2gf  6069  ofrval  6168  poxp  6317  smoel  6385  tfr1onlemaccex  6433  tfrcllemaccex  6446  nnaass  6570  qsel  6698  xpdom3m  6928  phpm  6961  ctssdc  7214  mkvprop  7259  prarloclem3  7609  aptisr  7891  axpre-apti  7997  axapti  8142  addn0nid  8445  divvalap  8746  letrp1  8920  p1le  8921  zextle  9463  zextlt  9464  btwnnz  9466  gtndiv  9467  uzind2  9484  fzind  9487  iccleub  10052  uzsubsubfz  10168  elfz0fzfz0  10247  difelfznle  10256  elfzo0le  10307  fzonmapblen  10309  fzofzim  10310  fzosplitprm1  10361  rebtwn2zlemstep  10393  qbtwnxr  10398  icogelb  10406  expcl2lemap  10694  expclzaplem  10706  expnegzap  10716  leexp2r  10736  expnbnd  10806  bcval4  10895  bccmpl  10897  elovmpowrd  11033  ccatval2  11052  absexpzap  11333  divalgb  12178  ndvdssub  12183  dvdsgcd  12275  dfgcd2  12277  rplpwr  12290  nnmindc  12297  lcmgcdlem  12341  coprmdvds1  12355  qredeq  12360  prmdvdsexpr  12414  nnnn0modprm0  12520  pcexp  12574  difsqpwdvds  12603  prmpwdvds  12620  elrestr  13021  isnmgm  13134  grpasscan1  13337  grpinvnz  13345  mulgneg2  13434  dvdsrmul1  13806  dvdsunit  13816  lmodlema  13996  mopni  14896  sincosq1lem  15239  rpcxpmul2  15327  logbgcd1irr  15381  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem4  15483  2lgsoddprmlem3  15530