Theorem 3impib 1134

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3impia  1135  mob  3675  eqreu  3687  dedth3h  4543  prproe  4865  rbropap  5538  breldmg  5891  ssimaexg  6963  funopdmsn  7146  fpr3g  8287  wfr3g  8321  dfsmo2  8339  omwordri  8564  3ecoptocl  8814  ttrclselem2  9711  frr3g  9744  r1filimi  9884  cfslb  10325  cofsmo  10328  cfsmolem  10329  coftr  10332  domtriomlem  10501  zorn2lem7  10561  ttukey2g  10575  gchi  10690  tskxpss  10838  tskord  10846  infm3  12257  uzind  12772  fzind  12778  fnn0ind  12779  xltnegi  13327  axdc4uz  14107  facwordi  14413  swrdnd2  14785  cshwidxmod  14934  relexpsucl  15164  relexpsucr  15165  relexprelg  15171  relexpaddnn  15184  caubnd  15506  mulgcd  16701  lcmfdvds  16797  lcmfdvdsb  16798  coprmdvds1  16807  pcfac  17057  ramz  17183  imasleval  17693  cictr  17960  initoeu2lem1  18169  drsdir  18456  psasym  18730  pstr  18731  tsrlin  18739  dirge  18757  mgmcl  18799  mgmhmlin  18868  issubmgm2  18872  mhmlin  18968  mhmmulg  19305  issubg2  19332  nsgbi  19347  gsumcom2  20169  srgmulgass  20423  dvdsrtr  20578  rnghmmul  20659  issubrng2  20790  issubrg2  20824  domnmuln0  20941  drnginvrcl  20991  drnginvrn0  20992  drnginvrl  20994  drnginvrr  20995  isdrngd  21002  isdrngdOLD  21004  abvmul  21058  abvtri  21059  lmhmlin  21290  ipcj  21920  cssincl  21974  obsip  22007  decpmatmulsumfsupp  23071  mp2pm2mplem4  23107  pm2mpghm  23114  pm2mpmhmlem1  23116  inopn  23197  basis1  23248  iscldtop  23393  2ndcdisj  23755  cnmpt2t  23972  cnmpt22  23973  cnmptcom  23977  fbasssin  24135  ptcmplem3  24353  xmeteq0  24637  prdsxmslem2  24828  nmvs  24975  nmolb  25016  volfiniun  25848  sincosq1sgn  26809  sincosq2sgn  26810  sincosq3sgn  26811  sincosq4sgn  26812  addsproplem2  28338  negsproplem2  28397  negsid  28409  mulsproplem9  28492  precsexlem10  28584  uzsind  28773  recut  28862  ewlkle  30168  wwlksnext  30464  umgr2adedgwlklem  30515  elwwlks2ons3im  30525  usgrwwlks2on  30529  umgrwwlks2on  30530  conngrv2edg  30778  frgrwopregasn  30899  frgrwopregbsn  30900  frgrwopreglem5  30904  frgrwopreglem5ALT  30905  frgr2wwlkeu  30910  ablocom  31132  nmcvcn  31279  ipassi  31425  htth  31502  shaddcl  31801  shmulcl  31802  shsubcl  31804  chlimi  31818  pjspansn  32161  cnopc  32497  cnfnc  32514  adj1  32517  lnfnmul  32632  atord  32972  atcvat2  32973  cdj3i  33025  nexple  33406  signstfvc  35186  bnj910  35561  bnj1154  35612  pconncn  35958  mrsubccat  36252  shftvalg  36466  linethru  36888  sin2h  38501  cos2h  38502  tan2h  38503  dvasin  38590  areacirclem1  38594  riotasv  39984  lsmsatcv  40035  omllaw  40268  2llnjN  40592  dalawlem10  40905  dalawlem13  40908  dalawlem14  40909  pclfinclN  40975  ismrc  43665  fzsplit1nn0  43718  pell1234qrmulcl  43815  pell14qrmulcl  43823  onsucf1olem  44230  iunrelexp0  44661  bi23impib  45428  bi13impib  45429  trelded  45507  suctrALT  45767  suctrALTcf  45863  suctrALTcfVD  45864  stoweidlem17  46971  zm1nn  48316  bgoldbtbndlem4  48850  bgoldbtbnd  48851  tgblthelfgott  48857  vopnbgrelself  48897  clnbgr3stgrgrlic  49062  clcllaw  49232  ztprmneprm  49403  lcoel0  49484  linindslinci  49504  fv2arycl  49704