Theorem 3impib 1116

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 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  3impia  1117  mob  3677  eqreu  3689  dedth3h  4537  prproe  4856  rbropap  5506  breldmg  5852  ssimaexg  6909  funopdmsn  7084  fpr3g  8218  wfr3g  8252  dfsmo2  8270  omwordri  8490  3ecoptocl  8736  ttrclselem2  9622  frr3g  9652  cfslb  10160  cofsmo  10163  cfsmolem  10164  coftr  10167  domtriomlem  10336  zorn2lem7  10396  ttukey2g  10410  gchi  10518  tskxpss  10666  tskord  10674  infm3  12084  uzind  12568  fzind  12574  fnn0ind  12575  xltnegi  13118  axdc4uz  13891  facwordi  14196  swrdnd2  14562  cshwidxmod  14709  relexpsucl  14938  relexpsucr  14939  relexprelg  14945  relexpaddnn  14958  caubnd  15266  mulgcd  16459  lcmfdvds  16553  lcmfdvdsb  16554  coprmdvds1  16563  pcfac  16811  ramz  16937  imasleval  17445  cictr  17712  initoeu2lem1  17921  drsdir  18208  psasym  18482  pstr  18483  tsrlin  18491  dirge  18509  mgmcl  18517  mgmhmlin  18573  issubmgm2  18577  mhmlin  18667  mhmmulg  18994  issubg2  19020  nsgbi  19036  gsumcom2  19854  srgmulgass  20102  dvdsrtr  20253  rnghmmul  20334  issubrng2  20443  issubrg2  20477  domnmuln0  20594  drnginvrcl  20638  drnginvrn0  20639  drnginvrl  20641  drnginvrr  20642  isdrngd  20650  isdrngdOLD  20652  abvmul  20706  abvtri  20707  lmhmlin  20939  ipcj  21541  cssincl  21595  obsip  21628  decpmatmulsumfsupp  22658  mp2pm2mplem4  22694  pm2mpghm  22701  pm2mpmhmlem1  22703  inopn  22784  basis1  22835  iscldtop  22980  2ndcdisj  23341  cnmpt2t  23558  cnmpt22  23559  cnmptcom  23563  fbasssin  23721  ptcmplem3  23939  xmeteq0  24224  prdsxmslem2  24415  nmvs  24562  nmolb  24603  volfiniun  25446  sincosq1sgn  26405  sincosq2sgn  26406  sincosq3sgn  26407  sincosq4sgn  26408  ssltsn  27703  addsproplem2  27882  negsproplem2  27940  negsid  27952  mulsproplem9  28032  precsexlem10  28123  uzsind  28298  recut  28365  0reno  28366  ewlkle  29551  wwlksnext  29838  umgr2adedgwlklem  29889  elwwlks2ons3im  29899  umgrwwlks2on  29902  conngrv2edg  30139  frgrwopregasn  30260  frgrwopregbsn  30261  frgrwopreglem5  30265  frgrwopreglem5ALT  30266  frgr2wwlkeu  30271  ablocom  30492  nmcvcn  30639  ipassi  30785  htth  30862  shaddcl  31161  shmulcl  31162  shsubcl  31164  chlimi  31178  pjspansn  31521  cnopc  31857  cnfnc  31874  adj1  31877  lnfnmul  31992  atord  32332  atcvat2  32333  cdj3i  32385  nexple  32790  signstfvc  34548  bnj910  34921  bnj1154  34972  umgr2cycllem  35123  pconncn  35207  mrsubccat  35501  shftvalg  35715  linethru  36137  sin2h  37600  cos2h  37601  tan2h  37602  dvasin  37694  areacirclem1  37698  riotasv  38948  lsmsatcv  38999  omllaw  39232  2llnjN  39556  dalawlem10  39869  dalawlem13  39872  dalawlem14  39873  pclfinclN  39939  ismrc  42684  fzsplit1nn0  42737  pell1234qrmulcl  42838  pell14qrmulcl  42846  onsucf1olem  43253  iunrelexp0  43685  bi23impib  44470  bi13impib  44471  trelded  44549  suctrALT  44809  suctrALTcf  44905  suctrALTcfVD  44906  stoweidlem17  46008  zm1nn  47296  bgoldbtbndlem4  47802  bgoldbtbnd  47803  tgblthelfgott  47809  vopnbgrelself  47849  clnbgr3stgrgrlic  48014  clcllaw  48185  ztprmneprm  48341  lcoel0  48423  linindslinci  48443  fv2arycl  48643