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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3impia  1117  mob  3678  eqreu  3690  dedth3h  4551  prproe  4868  rbropap  5527  breldmg  5870  ssimaexg  6932  funopdmsn  7101  fpr3g  8221  wfr3g  8258  dfsmo2  8298  omwordri  8524  3ecoptocl  8755  ttrclselem2  9671  frr3g  9701  cfslb  10211  cofsmo  10214  cfsmolem  10215  coftr  10218  domtriomlem  10387  zorn2lem7  10447  ttukey2g  10461  gchi  10569  tskxpss  10717  tskord  10725  infm3  12123  uzind  12604  fzind  12610  fnn0ind  12611  xltnegi  13145  axdc4uz  13899  facwordi  14199  swrdnd2  14555  cshwidxmod  14703  relexpsucl  14928  relexpsucr  14929  relexprelg  14935  relexpaddnn  14948  caubnd  15255  mulgcd  16440  lcmfdvds  16529  lcmfdvdsb  16530  coprmdvds1  16539  pcfac  16782  ramz  16908  imasleval  17437  cictr  17702  initoeu2lem1  17914  drsdir  18205  psasym  18479  pstr  18480  tsrlin  18488  dirge  18506  mgmcl  18514  mhmlin  18623  mhmmulg  18931  issubg2  18957  nsgbi  18973  gsumcom2  19766  srgmulgass  19962  dvdsrtr  20095  drnginvrcl  20246  drnginvrn0  20247  drnginvrl  20249  drnginvrr  20250  isdrngd  20255  isdrngdOLD  20257  issubrg2  20290  abvmul  20344  abvtri  20345  lmhmlin  20553  domnmuln0  20805  ipcj  21075  cssincl  21129  obsip  21164  decpmatmulsumfsupp  22159  mp2pm2mplem4  22195  pm2mpghm  22202  pm2mpmhmlem1  22204  inopn  22285  basis1  22337  iscldtop  22483  2ndcdisj  22844  cnmpt2t  23061  cnmpt22  23062  cnmptcom  23066  fbasssin  23224  ptcmplem3  23442  xmeteq0  23728  prdsxmslem2  23922  nmvs  24077  nmolb  24118  volfiniun  24948  sincosq1sgn  25892  sincosq2sgn  25893  sincosq3sgn  25894  sincosq4sgn  25895  addsproplem2  27325  negsproplem2  27370  negsid  27382  mulsproplem10  27431  ewlkle  28616  wwlksnext  28901  umgr2adedgwlklem  28952  elwwlks2ons3im  28962  umgrwwlks2on  28965  conngrv2edg  29202  frgrwopregasn  29323  frgrwopregbsn  29324  frgrwopreglem5  29328  frgrwopreglem5ALT  29329  frgr2wwlkeu  29334  ablocom  29553  nmcvcn  29700  ipassi  29846  htth  29923  shaddcl  30222  shmulcl  30223  shsubcl  30225  chlimi  30239  pjspansn  30582  cnopc  30918  cnfnc  30935  adj1  30938  lnfnmul  31053  atord  31393  atcvat2  31394  cdj3i  31446  nexple  32697  signstfvc  33275  bnj910  33649  bnj1154  33700  umgr2cycllem  33821  pconncn  33905  mrsubccat  34199  shftvalg  34390  linethru  34814  sin2h  36141  cos2h  36142  tan2h  36143  dvasin  36235  areacirclem1  36239  riotasv  37494  lsmsatcv  37545  omllaw  37778  2llnjN  38103  dalawlem10  38416  dalawlem13  38419  dalawlem14  38420  pclfinclN  38486  ismrc  41082  fzsplit1nn0  41135  pell1234qrmulcl  41236  pell14qrmulcl  41244  onsucf1olem  41663  iunrelexp0  42096  bi23impib  42889  bi13impib  42890  trelded  42969  suctrALT  43230  suctrALTcf  43326  suctrALTcfVD  43327  stoweidlem17  44378  zm1nn  45654  bgoldbtbndlem4  46120  bgoldbtbnd  46121  tgblthelfgott  46127  mgmhmlin  46200  issubmgm2  46204  clcllaw  46245  rnghmmul  46318  ztprmneprm  46543  lcoel0  46629  linindslinci  46649  fv2arycl  46854