Theorem 3impia 1117

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1116	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:  mopick2  2630  ceqsalt  3478  3gencl  3488  vtoclgft  3515  vtoclegft  3551  rspc6v  3606  mob2  3683  moi  3686  reupick3  4289  disjne  4414  elpr2elpr  4829  disji2  5086  disji  5087  tz7.2  5614  sofld  6148  ordintdif  6371  funopg  6534  fvun1  6934  fvopab6  6984  fveqressseq  7033  fvcofneq  7047  fprg  7109  isores3  7292  ovmpt4g  7516  ovmpos  7517  ov2gf  7518  ofrval  7645  sorpssuni  7688  sorpssint  7689  poxp  8084  poseq  8114  suppss2  8156  frrlem12  8253  smoel  8306  smoord  8311  smogt  8313  oaass  8502  oewordi  8532  oeoalem  8537  oeoelem  8539  nnawordi  8562  nnaass  8563  naddssim  8626  qsel  8746  xpdom3  9016  onsdominel  9067  mapdom3  9090  sdomdomtrfi  9142  domsdomtrfi  9143  php  9148  onomeneq  9155  fisseneq  9180  fodomfir  9255  cantnflem1  9618  ttrclss  9649  cfslbn  10196  cfsmolem  10199  cfcoflem  10201  infpssrlem4  10235  fin23lem7  10245  fin23lem25  10253  isf34lem7  10308  hsmexlem2  10356  axcc3  10367  axdc4lem  10384  tskss  10687  gruss  10725  gruurn  10727  gruiun  10728  gruel  10732  gruen  10741  grudomon  10746  grothac  10759  axpre-sup  11098  axsup  11225  addn0nid  11574  letrp1  12002  p1le  12003  lemul1a  12012  infrelb  12144  zextle  12583  zextlt  12584  btwnnz  12586  gtndiv  12587  uzind2  12603  fzind  12608  eluzsubOLD  12805  zsupss  12872  xrltne  13099  lemaxle  13131  qbtwnre  13135  qbtwnxr  13136  xlemul1a  13224  icogelb  13333  iccleub  13338  iccsplit  13422  uzsubsubfz  13483  elfz0fzfz0  13570  difelfznle  13579  fvffz0  13583  elfzo0le  13640  fzonmapblen  13645  fzofzim  13646  ceile  13787  modadd1  13846  muladdmodid  13851  modmul1  13865  modirr  13883  fsuppmapnn0fiub0  13934  expcl2lem  14014  expclzlem  14024  expnegz  14037  leexp2r  14115  bcval4  14248  bccmpl  14250  hashbnd  14277  hashunsnggt  14335  hashgt23el  14365  hashfundm  14383  elovmpowrd  14499  ccatval2  14519  ccatrcl1  14535  wrdl1s1  14555  ccat2s1fvw  14579  swrdsb0eq  14604  swrdccatin1  14666  pfxccatpfx2  14678  repswswrd  14725  cshwcsh2id  14770  absexpz  15247  climbdd  15614  iseraltlem2  15625  binomfallfac  15983  dvdsle  16256  divalgb  16350  ndvdssub  16355  dvdsgcd  16490  dfgcd2  16492  rplpwr  16504  nn0rppwr  16507  nn0expgcd  16510  lcmgcdlem  16552  lcmfunsn  16590  coprmdvds1  16598  qredeq  16603  2mulprm  16639  prmdvdsexpr  16663  nnnn0modprm0  16753  prm23ge5  16762  pcexp  16806  difsqpwdvds  16834  prmpwdvds  16851  ramcl  16976  cshwshashlem3  17044  cshwrepswhash1  17049  elrestr  17367  mreintcl  17532  mremre  17541  mrieqv2d  17576  initoeu2lem1  17952  funcestrcsetclem9  18085  funcsetcestrclem9  18100  prstr  18236  drsdirfi  18242  latnlej  18391  latnlej2  18394  acsdrsel  18478  acsdrscl  18481  mrelatglb  18495  mrelatlub  18497  isnmgm  18547  grpasscan1  18909  grpinvnz  18918  mulgneg2  19016  gsmsymgrfix  19334  f1omvdco2  19354  symggen  19376  odcl2  19471  odhash3  19482  lsmss1  19571  lsmss2  19573  efgred  19654  efgcpbl  19662  ablfacrp  19974  ablfac1eu  19981  ablfaclem3  19995  dvdsrmul1  20254  dvdsunit  20264  irredmul  20314  c0snmgmhm  20347  lmodlema  20747  psgnodpmr  21475  phlssphl  21544  lindsss  21709  lindfmm  21712  ply1scln0  22154  dmatelnd  22359  mdetdiaglem  22461  mdet0  22469  mdetunilem7  22481  slesolinv  22543  cramerimplem3  22548  cpmatpmat  22573  m2cpminvid2lem  22617  chfacfscmul0  22721  chfacfpmmul0  22725  riinopn  22771  clsndisj  22938  cnpf2  23113  hausnei2  23216  cmpcov  23252  cmpfii  23272  unconn  23292  t1connperf  23299  nrmr0reg  23612  fbfinnfr  23704  filuni  23748  alexsubALT  23914  tmdgsum  23958  cuspcvg  24164  mopni  24356  isngp4  24476  metdsre  24718  iimulcl  24809  phtpc01  24871  clmmulg  24977  cfilucfil4  25197  bcthlem5  25204  bcth  25205  bcth3  25207  itg1le  25590  itg2le  25616  bddmulibl  25716  bddiblnc  25719  dvnres  25809  cpnord  25813  dvnfre  25832  deg1ge  25979  dgr1term  26141  aaliou3lem2  26227  sincosq1lem  26382  cxpge0  26568  cxpmul2  26574  logrec  26649  logbgcd1irr  26680  sqfpc  27023  bcmono  27164  gausslemma2dlem1a  27252  gausslemma2dlem2  27254  gausslemma2dlem4  27256  2lgsoddprmlem3  27301  pntrmax  27451  qabvexp  27513  ostth2lem2  27521  nosepon  27553  nolesgn2o  27559  nogesgn1o  27561  nosepnelem  27567  nosepne  27568  nosepdmlem  27571  nosepdm  27572  nodenselem8  27579  noresle  27585  noetasuplem4  27624  noetainflem4  27628  scutbdaylt  27706  addsuniflem  27884  ssltmul1  28026  precsexlem6  28090  precsexlem7  28091  precsexlem11  28095  sltonold  28138  onnolt  28143  n0sfincut  28222  expadds  28296  ax5seglem4  28835  axeuclidlem  28865  uhgredgrnv  29033  usgredg4  29120  nbuhgr2vtx1edgblem  29254  vtxduhgr0e  29382  vtxduhgr0nedg  29396  rusgrpropnb  29487  uspgr2wlkeqi  29551  redwlklem  29573  lfgrwlkprop  29589  2pthnloop  29634  spthonepeq  29655  pthdlem2lem  29670  crctcshwlkn0lem3  29715  crctcshwlkn0lem5  29717  crctcshwlkn0lem7  29719  crctcshwlkn0  29724  wlkiswwlks1  29770  wlkiswwlks2  29778  wlkiswwlksupgr2  29780  wwlksnext  29796  wwlksnextproplem2  29813  wspthsnonn0vne  29820  2pthon3v  29846  rusgrnumwwlk  29878  erclwwlkeqlen  29921  erclwwlksym  29923  erclwwlktr  29924  erclwwlkneqlen  29970  erclwwlknsym  29972  erclwwlkntr  29973  uhgr3cyclex  30084  upgreupthseg  30111  eupth2lem3lem4  30133  eucrctshift  30145  4cycl2vnunb  30192  nvs  30565  nvtri  30572  nmlno0  30697  nmlnoubi  30698  ubth  30775  hlipgt0  30816  ocnel  31200  elspansn2  31469  elspansn3  31474  normcan  31478  pjoml2  31513  lecm  31519  osum  31547  nmbdfnlb  31952  leopmul  32036  hstpyth  32131  cvnbtwn  32188  ssmd1  32213  ssmd2  32214  ssdmd1  32215  ssdmd2  32216  cvmd  32238  cvdmd  32239  superpos  32256  disji2f  32479  disjif  32480  disjif2  32483  preiman0  32606  padct  32616  ffs2  32624  bcm1n  32691  sgn3da  32732  s2f1  32839  omndadd  32993  ogrpaddlt  33004  archiabl  33125  slmdlema  33129  lbslsat  33585  eulerpartlemb  34332  fisshasheq  35075  cvmsdisj  35230  cvmlift2lem12  35274  satfrel  35327  satfrnmapom  35330  fmlasuc  35346  satffun  35369  satef  35376  sategoelfv  35380  lineintmo  36118  nn0prpwlem  36283  nn0prpw  36284  neibastop2lem  36321  lindsadd  37580  areacirc  37680  incsequz  37715  mettrifi  37724  ismtybnd  37774  heiborlem1  37778  rngoisocnv  37948  risci  37954  eqvrelqsel  38580  lfl1  39036  lkrlsp2  39069  omlfh3N  39225  cvrnbtwn  39237  cvrnbtwn2  39241  cvrnbtwn4  39245  cvlexch3  39298  cvlexch4N  39299  cvlatexchb1  39300  2llnne2N  39375  atcvrj0  39395  cvrat2  39396  ps-1  39444  3atlem5  39454  islln2a  39484  lplnriaN  39517  lplnribN  39518  llncvrlpln2  39524  lplncvrlvol2  39582  psubatN  39722  pmapglb2N  39738  pmapglb2xN  39739  2llnma1b  39753  paddasslem17  39803  pmod2iN  39816  pmodl42N  39818  hlmod1i  39823  atmod1i1  39824  atmod1i2  39826  llnmod1i2  39827  pclcmpatN  39868  osumcllem8N  39930  pexmidlem3N  39939  pl42lem4N  39949  4atexlem7  40042  ltrnnid  40103  cdlemc4  40161  cdleme32a  40408  cdlemeg46gfre  40499  cdlemf2  40529  cdlemg4c  40579  trlcoat  40690  tendovalco  40732  tendoeq2  40741  cdlemk36  40880  diael  41010  diatrl  41011  dicelval1stN  41155  dicelval2nd  41156  dihlspsnat  41300  dochkr1  41445  lcfrlem9  41517  mapdh8e  41751  hdmapval0  41800  hgmapval0  41859  nnadddir  42231  dvdsexpnn0  42295  incssnn0  42672  pell14qrexpcl  42828  pell14qrgap  42836  congadd  42928  acongsym  42938  acongtr  42940  dvdsacongtr  42946  jm2.19lem3  42953  jm2.19lem4  42954  jm2.26lem3  42963  onexlimgt  43205  nadd2rabex  43348  ismnushort  44263  bi13impia  44452  3impcombi  44779  ioogtlb  45466  iocgtlb  45473  iocleub  45474  icoltub  45479  iooltub  45481  limclner  45622  limsupre3lem  45703  climuzlem  45714  fsupdm  46813  finfdm  46817  elfzelfzlble  47295  subsubelfzo0  47300  m1modnep2mod  47326  m1modmmod  47332  modlt0b  47337  mod2addne  47338  iccpartigtl  47397  sqrtpwpw2p  47512  fmtnoprmfac1lem  47538  fmtno4prmfac  47546  evenltle  47691  even3prm2  47693  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbndlem1  47779  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  bgoldbtbnd  47783  uhgrimisgrgriclem  47903  isubgr3stgrlem7  47944  clnbgr3stgrgrlic  47984  gpgedg2iv  48031  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  upgrwlkupwlk  48101  funcringcsetcALTV2lem9  48259  funcringcsetclem9ALTV  48282  lincscmcl  48394  lindslinindimp2lem4  48423  lincresunit2  48440  lincresunit3  48443  elfzolborelfzop1  48481  rege1logbzge0  48521  fllog2  48530  dignn0ldlem  48564  rrx2pnecoorneor  48677  rrx2plord2  48684  rrx2linest  48704  ipolub  48949  ipoglb  48952