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  3678  eqreu  3690  dedth3h  4546  prproe  4836  rbropap  5542  breldmg  5898  ssimaexg  6994  funopdmsn  7178  fpr3g  8331  wfr3g  8365  dfsmo2  8383  omwordri  8608  3ecoptocl  8858  ttrclselem2  9754  frr3g  9787  r1filimi  9930  cfslb  10371  cofsmo  10374  cfsmolem  10375  coftr  10378  domtriomlem  10547  zorn2lem7  10607  ttukey2g  10621  gchi  10736  tskxpss  10884  tskord  10892  infm3  12303  uzind  12818  fzind  12824  fnn0ind  12825  xltnegi  13373  axdc4uz  14154  facwordi  14460  swrdnd2  14833  cshwidxmod  14982  relexpsucl  15213  relexpsucr  15214  relexprelg  15220  relexpaddnn  15233  caubnd  15555  mulgcd  16750  lcmfdvds  16846  lcmfdvdsb  16847  coprmdvds1  16856  pcfac  17106  ramz  17232  imasleval  17742  cictr  18009  initoeu2lem1  18218  drsdir  18505  psasym  18779  pstr  18780  tsrlin  18788  dirge  18806  mgmcl  18848  mgmhmlin  18917  issubmgm2  18921  mhmlin  19017  mhmmulg  19354  issubg2  19381  nsgbi  19396  gsumcom2  20219  srgmulgass  20473  dvdsrtr  20628  rnghmmul  20709  issubrng2  20840  issubrg2  20874  domnmuln0  20991  drnginvrcl  21041  drnginvrn0  21042  drnginvrl  21044  drnginvrr  21045  isdrngd  21052  isdrngdOLD  21054  abvmul  21108  abvtri  21109  lmhmlin  21340  ipcj  21970  cssincl  22024  obsip  22057  decpmatmulsumfsupp  23121  mp2pm2mplem4  23157  pm2mpghm  23164  pm2mpmhmlem1  23166  inopn  23247  basis1  23298  iscldtop  23443  2ndcdisj  23805  cnmpt2t  24022  cnmpt22  24023  cnmptcom  24027  fbasssin  24185  ptcmplem3  24403  xmeteq0  24687  prdsxmslem2  24878  nmvs  25025  nmolb  25066  volfiniun  25898  sincosq1sgn  26857  sincosq2sgn  26858  sincosq3sgn  26859  sincosq4sgn  26860  addsproplem2  28386  negsproplem2  28445  negsid  28457  mulsproplem9  28540  precsexlem10  28632  uzsind  28821  recut  28910  ewlkle  30216  wwlksnext  30512  umgr2adedgwlklem  30563  elwwlks2ons3im  30573  usgrwwlks2on  30577  umgrwwlks2on  30578  conngrv2edg  30826  frgrwopregasn  30947  frgrwopregbsn  30948  frgrwopreglem5  30952  frgrwopreglem5ALT  30953  frgr2wwlkeu  30958  ablocom  31180  nmcvcn  31327  ipassi  31473  htth  31550  shaddcl  31849  shmulcl  31850  shsubcl  31852  chlimi  31866  pjspansn  32209  cnopc  32545  cnfnc  32562  adj1  32565  lnfnmul  32680  atord  33020  atcvat2  33021  cdj3i  33073  nexple  33494  signstfvc  35273  bnj910  35648  bnj1154  35699  acwer1prclem  35851  pconncn  36156  mrsubccat  36450  shftvalg  36675  linethru  37096  sin2h  38725  cos2h  38726  tan2h  38727  dvasin  38814  areacirclem1  38818  riotasv  40208  lsmsatcv  40259  omllaw  40492  2llnjN  40816  dalawlem10  41129  dalawlem13  41132  dalawlem14  41133  pclfinclN  41199  ismrc  43905  fzsplit1nn0  43958  pell1234qrmulcl  44055  pell14qrmulcl  44063  onsucf1olem  44464  iunrelexp0  44894  bi23impib  45660  bi13impib  45661  trelded  45739  suctrALT  45999  suctrALTcf  46095  suctrALTcfVD  46096  stoweidlem17  47232  zm1nn  48577  bgoldbtbndlem4  49111  bgoldbtbnd  49112  tgblthelfgott  49118  vopnbgrelself  49158  clnbgr3stgrgrlic  49323  clcllaw  49493  ztprmneprm  49664  lcoel0  49745  linindslinci  49765  fv2arycl  49965